/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.transl;

import alloy.ast.ArrowMultExpr;
import alloy.ast.ComprehensionExpr;
import alloy.ast.LeafId;
import alloy.ast.Multiplicity;
import alloy.ast.MultiplicityExpr;
import alloy.ast.SetMultExpr;
import alloy.bool.BoolSwitch;
import alloy.bool.BooleanFormula;
import alloy.type.RelationType;
import alloy.util.Dbg;
import alloy.util.MultiDimArray;
import alloy.util.Params;
import alloy.util.Util;

/**
 * Code for generating all values of a given quantified variable, based on the
 * variable's declaration.  (E.g. for a quantified variable x declared as "all x: A | ..."
 * we would generate the value sequence [{<A0>},{<A1>},{<A1>}] if the scope of A is 3).
 * This code is also {@linkplain DefaultRelationAllocator#_computeProductSigTransls "abused"}
 * for generating the translation of <a href="../../overview-summary.html#prodsig">product signatures</a>.
 * <p>
 * How the generated values are represented: we construct an {@link ExprTransl} consisting
 * of {@linkplain BooleanFormula#isConstantValued constant-valued} {@link BooleanFormula}s
 * that depend on {@linkplain alloy.bool.VarConst switchable constants} that depend on
 * a particular {@link alloy.bool.BoolSwitch}, and a sequence of <code>long</code> values
 * where each value corresponds to one relational value of the quantified variable --
 * assigning that value to the Boolean switch sets the switchable constants in the
 * ExprTransl in such as way that the ExprTransl represents the relational value
 * of the quantified variable.
 * 
 * @see TranslVisitor
 * @see QVarIterationInfo
 */
class QVarValGenerator {
    /**
     * Compute the information necessary to iterate through the values of the given
     * quantified variable.
     */
    static QVarIterationInfo constructQVarIterationInfo(LeafId leafId_, ASTInfo astInfo_) {
	Dbg.chk(astInfo_.isQuantVar(leafId_) || astInfo_.getRelations().contains(leafId_));
	boolean declaredInComprehension = astInfo_.isQuantVar(leafId_) &&
	    astInfo_.getVarCreator(leafId_) instanceof ComprehensionExpr;
	return constructQVarIterationInfo(astInfo_.getLeafType(leafId_),
					  astInfo_.getLeafMultiplicity(leafId_),
					  declaredInComprehension,
					  astInfo_.getLeafRep(leafId_).nodeString());
					  
    }
	
    /**
     * Compute the information necessary to iterate through the values of the given
     * quantified variable.
     */
    static QVarIterationInfo constructQVarIterationInfo(RelationType relType_,
							MultiplicityExpr multExpr_,
							boolean declaredInComprehension_,
							String varName_) {
	long[] boolSwitchValues; // each corresponds to one relational value to assign to the quantified variable
	int[][] oneTupleCoords = null;
	int funcDim = -1;
	boolean funcIsOptionMult = false;
	if (relType_.numBasicTypes() == 1) {
	    // quantified variable is set-valued
	    Multiplicity setMult = ((SetMultExpr)multExpr_).getMult();
	    int setScope = relType_.getBasicTypeAt(0).getScope();
	    if (declaredInComprehension_ ||
		setMult.equals(Multiplicity.NONE) ||
		setMult.equals(Multiplicity.ONE) ||
		setMult.equals(Multiplicity.LONE)) {
		if (Params.glob.getBoolParam("DEVEL", "compalloc")) {
            Dbg.info("The development option CompactAllocation is turned on. "
            + "It doesn't work right now: please turn it off.");
        }
		if (false && Params.glob.getBoolParam("DEVEL", "compalloc")) {
		    funcDim = 0;
		    funcIsOptionMult = 
			!declaredInComprehension_ && setMult.equals(Multiplicity.LONE);
		    boolSwitchValues = new long[setScope + (funcIsOptionMult ? 1 : 0)];
		    
		    for (int i=0; i<boolSwitchValues.length; i++)
			boolSwitchValues[i] = i;
		    
		    if (declaredInComprehension_) {
			oneTupleCoords = new int[boolSwitchValues.length][1];
			for (int i=0; i<boolSwitchValues.length; i++) {
			    oneTupleCoords[i][0] = i;
			}
		    }
		} else {

		    boolean isOption = 
			!declaredInComprehension_ && setMult.equals(Multiplicity.LONE);
		    
		    boolSwitchValues = new long[setScope + (isOption ? 1 : 0)];
		    int boolSwitchVal = 1;
		    for (int i=0; i<setScope; i++) {
			//Dbg.chk(boolSwitchVal > 0);
			boolSwitchValues[i] = boolSwitchVal;
			boolSwitchVal <<= 1;
		    }

		    if (isOption)
			boolSwitchValues[setScope] = 0;

		    if (declaredInComprehension_) {
			Dbg.chk(!isOption);
			oneTupleCoords = new int[boolSwitchValues.length][1];
			for (int i=0; i<boolSwitchValues.length; i++) {
			    oneTupleCoords[i][0] = i;
			}
		    }
		}
	    } else {
		// quantified variable ranges over all sets
		Dbg.chk(setMult.equals(Multiplicity.SET));
		int maxVal = (1 << setScope);
		Dbg.chk (maxVal > 0);
		boolSwitchValues = new long[maxVal];
		for (int i=0; i<maxVal; i++)
		    boolSwitchValues[i] = i;
	    }
	} else { // not a unary relation; arity at least 2

	    System.out.println("IN QVARVALGEN " + multExpr_.nodeString());
	    System.out.println(multExpr_.getParent().nodeString());
	    System.out.println(multExpr_.getClass());
	    ArrowMultExpr arrowMult = (ArrowMultExpr)multExpr_;
	    Multiplicity leftMult = arrowMult.getLeft().getMult();
	    Multiplicity rightMult = arrowMult.getRight().getMult();
	    
	    if (!declaredInComprehension_) {
		//Dbg.chk(false);
		
		// for now, just ground out for all possible values.
		// note that this works badly for vars declared in
		// comprehensions -- fix later.
		
		int maxVal = (1 << relType_.getNumTuples());
		Dbg.chk(maxVal > 0);
		boolSwitchValues = new long[maxVal];
		for (int i=0; i<maxVal; i++)
		    boolSwitchValues[i] = i;
	    } else {  // declaredInComprehension
		// each value will be a singleton, and multiplicity markings
		// will be ignored
		Dbg.chk(leftMult.equals(Multiplicity.NONE) &&
			rightMult.equals(Multiplicity.NONE));
		int ntuples = relType_.getNumTuples();
		boolSwitchValues = new long[ntuples];
		for (int i=0; i<ntuples; i++)
		    boolSwitchValues[i] = (1 << i);
	    }
	}  // arity >= 2

	int[] dims = (int[])relType_.getScopes().clone();
	Dbg.chk(funcDim == -1);
	if (funcDim >= 0) {
	    dims[funcDim] = Util.binaryLogUp(dims[funcDim] + (funcIsOptionMult ? 1 : 0));
	}
	MultiDimArray formulas = new MultiDimArray(dims);
	Object[] formulasFlat = formulas.getFlatData();
	Dbg.chk(formulasFlat.length < 64);
	BoolSwitch boolSwitch = new BoolSwitch(varName_);
	for (int i=0; i<formulasFlat.length; i++) {
	    formulasFlat[i] = BooleanFormula.makeSwitchableConst(boolSwitch, i);
	}
	ExprTransl qvarTransl =
	    funcDim>=0 ? new ExprTransl(relType_, formulas, funcDim, funcIsOptionMult) :
	    new ExprTransl(relType_, formulas);
	QVarIterationInfo result = new QVarIterationInfo(boolSwitch, boolSwitchValues, oneTupleCoords, qvarTransl);
	//System.out.println(result);
	return result;
    }  // constructQVarIterationInto()
}  // class QVarValGenerator

